f31ba263bb22a944bba521605b375d5d8b76fdbb,org.coreasm.engine/src/org/coreasm/engine/plugins/predicatelogic/PredicateLogicPlugin.java,PredicateLogicPlugin,interpretExists,#Interpreter#ASTNode#,385

Before Change


                	if (s == null) {
            			Enumerable domain = (Enumerable)variable.getValue().getValue();
            			if (domain.supportsIndexedView())
            				s = new ArrayList<Element>(domain.getIndexedView());
            			else
            				s = new ArrayList<Element>(((Enumerable) variable.getValue().getValue()).enumerate());
            			if (s.isEmpty()) {
                			for (Entry<String, ASTNode> var : variableMap.entrySet()) {
            	    			if (remained.remove(var.getValue()) != null)
            	    				interpreter.removeEnv(var.getKey());
            	    		}
            				// [pos] := (undef,undef,ff)
                			existsExpNode.setNode(null, null, BooleanElement.FALSE);
            	            return existsExpNode;
                    	}
            			remained.put(variable.getValue(), s);
                		shouldChoose = true;
                	}
                	else if (shouldChoose)
                		interpreter.removeEnv(variable.getKey());
                	
                	if (shouldChoose) {
	                    if (!s.isEmpty()) {
	                    	// SPEC: considered := considered union {t}
	                        // choose t in s, for simplicty choose the first 
	                        // since we have to go through all of them
	                        Element chosen = s.remove(0);
	                        shouldChoose = false;
	                        
	                        // SPEC: AddEnv(x,t)

After Change


                	if (it == null) {
            			Enumerable domain = (Enumerable)variable.getValue().getValue();
            			if (domain.supportsIndexedView())
            				it = domain.getIndexedView().iterator();
            			else
            				it = domain.enumerate().iterator();
            			if (!it.hasNext()) {
                			for (Entry<String, ASTNode> var : variableMap.entrySet()) {
            	    			if (iterators.remove(var.getValue()) != null)
            	    				interpreter.removeEnv(var.getKey());
            	    		}
            				// [pos] := (undef,undef,ff)
                			existsExpNode.setNode(null, null, BooleanElement.FALSE);
            	            return existsExpNode;
                    	}
            			iterators.put(variable.getValue(), it);
                		shouldChoose = true;
                	}
                	else if (shouldChoose)
                		interpreter.removeEnv(variable.getKey());
                	
                	if (shouldChoose) {
	                    if (it.hasNext()) {
	                    	// SPEC: considered := considered union {t}
	                        Element chosen = it.next();
	                        shouldChoose = false;
	                        
	                        // SPEC: AddEnv(x,t)